(set-logic QF_LRA)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(declare-fun v3 () Real)
(declare-fun v4 () Real)

(declare-fun b1 () Bool)
(declare-fun b2 () Bool)
(declare-fun b3 () Bool)
(declare-fun b4 () Bool)

(assert (= (+ v2 (ite b1 v2 v3)) v1))
(assert (= b2 (<= v4 v1)))
(assert (= b3 (not b2)))
(assert (= b4 (and b3 (not b1))))
(assert b4)
(assert (distinct v2 v3))
(check-sat)
